PACKAGE BODY IntSqrt IS

   PROCEDURE IntSqrtBis (M: OUT Integer; N: in Integer) IS
      Li: Integer;
      Re: Integer;
   BEGIN
      --#PRE: N = N_anf AND N >= 2
      Li := 0;
      Re := N;

      --#BOUND: Re-(Li+1)
      --#INV: (Li**2) <= N AND N < (Re**2) AND Li < Re
      WHILE (Li+1) < Re LOOP
         M := ((Li+Re)/2);
         --#Q: (Li**2) <= N AND N < (Re**2) AND Li < Re AND M = ((Li+Re)/2)
         IF (M**2) <= N THEN
            Li := M;
         ELSE
            Re := M;
         END IF;
      END LOOP;
      --#POST: (M**2) <= N AND N < ((M+1)**2)
   END IntSqrtBis;

   PROCEDURE IntSqrtLin (X: IN Integer; A: OUT Integer) IS
      B, C: Integer;
   BEGIN
      --#PRE: X >= 0
      A := 0;
      B := 1;
      C := 1;
      --#BOUND: (X-B)+C
      --#INV: (A**2) <= X AND B = ((A+1)**2) AND C = ((A+A)+1) AND A >= 0
      WHILE B <= X LOOP
         A := (A+1);
         C := (C+2);
         B := (B+C);
      END LOOP;
      --#POST: (A**2) <= X AND X < ((A+1)**2)
   END IntSqrtLin;

END IntSqrt;
